\documentclass[11pt]{article}

\usepackage{multicol}
\usepackage{algorithmic}[5]
\usepackage{algorithm}
\usepackage{amsmath, amsthm, amssymb}
\usepackage{cite}
\usepackage{url}

\setlength{\topmargin}{0in}
\setlength{\headheight}{0cm}
\setlength{\headsep}{0cm}
\setlength{\textheight}{9in}
\setlength{\oddsidemargin}{0cm}
\setlength{\evensidemargin}{0cm}
\setlength{\textwidth}{6.5in}

\renewcommand{\algorithmiccomment}[1]{// #1}
\renewcommand{\algorithmicensure}{\textbf{define}}
\newcommand{\ttype}[1]{\textsf{#1}}
\newcommand{\mtype}[1]{\mathsf{#1}}
\newcommand{\tfn}[1]{\textbf{#1}}
\newcommand{\mfn}[1]{\mathbf{#1}}
\newcommand{\ttr}{\texttt{true}}
\newcommand{\mtr}{\mathtt{true}}
\newcommand{\tfl}{\texttt{false}}
\newcommand{\mfl}{\mathtt{false}}

\begin{document}

\title{Design and Implementation of a\\
Hybrid-Typed Programming Language}

\def\to{\rightarrow}
\def\evals{\mapsto}

\author{Michael M. Vitousek\\
Willamette University\\
\texttt{mvitouse@willamette.edu}}
\date{\today}
\maketitle

\section{Syntax}
For any $a$, $a^*$ is the Kleene star (that is, $a$ repeated any number of times), and $a^+$ is $a(a^*)$ (that is, $a$ repeated one or more times).
\subsection{Terms}
\begin{tabular}{rll|l}
$t$ & $::=$ & $x$ & variables \\
& & $c$ & constants \\
& & let $(x=t:T)^+$ in $t$ & binding (in new scope)\\
& & define $(x=t:T)^+$ & binding (in same scope)\\
& & match $t$ with $(p, t)^*$, default $t$ & pattern matching \\
& & match-dyn $t$ $(p, t)^*$, default $t$ & un-typechecked pattern matching \\
& & if $t$ then $t$ else $t$ & conditional \\
& & if-dyn $t$ then $t$ else $t$ & un-typechecked conditional \\
& & $\lambda (x:T)^*.t$ & abstraction \\
& & $t\;t^*$ & application \\
& & $t \mid t$ & sequencing \\
\end{tabular}
\subsection{Patterns}
\begin{tabular}{rll|l}
$p$ & $::=$ & $\texttt{nil}$ & matches the empty list \\
& & $x\;p$ & matches an element of the list followed by another pattern
\end{tabular}
\subsection{Values}
\begin{tabular}{rll|l}
$v$ & $::=$ & $c$ & constants \\
& & $\lambda (x:T)^*.t$ & abstractions \\
\end{tabular}
\subsection{Types}
\begin{tabular}{rll|l}
$T$ & $::=$ & \ttype{Int} & $\{n \mid n \in \mathbb{Z}\}$ \\
& & \ttype{Real} & $\{n \mid n \in \mathbb{R}\}$ \\
& & \ttype{Boolean} & $\{\mtr, \mfl\}$ \\
& & \ttype{Char} & $\{n \mid n \in \mathtt{ascii}\}$ \\
& & \ttype{Nil} & $\emptyset$ \\
& & $[T]$  & lists of $T$ \\
& & $[T \times T]$ & pairs \\
& & $[T \times T \times \cdots \times T \to T]$ & function types \\
& & \ttype{Dynamic} & type unchecked \\
\end{tabular}
\subsection{Constants}
\begin{tabular}{rll|l}
$c$ & $::=$ & $\mathtt{nil} : \mtype{Nil}$ & \\
& & $\mtr : \mtype{Boolean}$ & \\
& & $\mfl : \mtype{Boolean}$ & \\
& & $n \in \mathbb{Z} : \mtype{Int}$ & \\
& & $n \in \mathbb{R} : \mtype{Real}$ & \\
& & $\textsc{I-NaN} : \mtype{Int}$ & \\
& & $\textsc{R-NaN} : \mtype{Real}$ & \\
& & $n \in \mathtt{ascii} : \mtype{Char}$ & \\
& & $\mfn{neg} : [\tau \to \tau]$ & $\tau \in \{\mtype{Int}, \mtype{Real}\}$ \\
& & $\mfn{add} : [\tau \times \tau \to \tau]$ & $\tau \in \{\mtype{Int}, \mtype{Real}\}$ \\
& & $\mfn{sub} : [\tau \times \tau \to \tau]$ & $\tau \in \{\mtype{Int}, \mtype{Real}\}$ \\
& & $\mfn{mult} : [\tau \times \tau \to \tau]$ & $\tau \in \{\mtype{Int}, \mtype{Real}\}$ \\
& & $\mfn{div} : [\tau \times \tau \to \tau]$ & $\tau \in \{\mtype{Int}, \mtype{Real}\}$ \\
& & $\mfn{exp} : [\tau \times \tau \to \tau]$ & $\tau \in \{\mtype{Int}, \mtype{Real}\}$ \\
& & $\mfn{mod} : [\mtype{Int} \times \mtype{Int} \to \mtype{Int}]$ & \\
& & $\mfn{fact} : [\mtype{Int} \to \mtype{Int}]$ & \\
& & $\mfn{gt} : [\tau \times \tau \to \mtype{Boolean}]$ & $\tau \in \{\mtype{Int}, \mtype{Real}\}$ \\
& & $\mfn{lt} : [\tau \times \tau \to \mtype{Boolean}]$ & $\tau \in \{\mtype{Int}, \mtype{Real}\}$ \\
& & $\mfn{ge} : [\tau \times \tau \to \mtype{Boolean}]$ & $\tau \in \{\mtype{Int}, \mtype{Real}\}$ \\
& & $\mfn{le} : [\tau \times \tau \to \mtype{Boolean}]$ & $\tau \in \{\mtype{Int}, \mtype{Real}\}$ \\
& & $\mfn{eq} : [\tau \times \tau \to \mtype{Boolean}]$ & $\tau \in T$ \\
& & $\mfn{neq} : [\tau \times \tau \to \mtype{Boolean}]$ & $\tau \in T$ \\
& & $\mfn{and} : [\mtype{Boolean} \times \mtype{Boolean} \to \mtype{Boolean}]$ & \\
& & $\mfn{or} : [\mtype{Boolean} \times \mtype{Boolean} \to \mtype{Boolean}]$ & \\
& & $\mfn{not} : [\mtype{Boolean} \to \mtype{Boolean}]$ & \\
& & $\mfn{cons} : [\tau_1 \times \tau_2 \to [\tau_1 \times \tau_2]]$ & $\tau_1, \tau_2 \in T$ \\
& & $\mfn{attach} : [\tau \times [\tau] \to [\tau]]$ & $\tau \in T$ \\
& & $\mfn{car} : [[\tau_1 \times \tau_2] \to \tau_1]$ & $\tau_1, \tau_2 \in T$ \\
& & $\mfn{cdr} : [[\tau_1 \times \tau_2] \to \tau_2]$ & $\tau_1, \tau_2 \in T$ \\
& & $\mfn{print} : [[\mtype{Char}] \to \mtype{Nil}]$ & \\
& & $\mfn{read} : [\mtype{Nil} \to [\mtype{Char}]]$ & \\
& & $\mfn{eval} : [[\mtype{Char}] \to \mtype{Dynamic}]$ & \\

\end{tabular}

\section{Evaluation Rules}
For any $a$, $a^n$ is $n$ repetitions of $a$ (i.e., $a^2$ is $aa$). The term $p \models v$ may be read as ``the pattern $p$ successfully matches the value $v$.''
The symbol $\Gamma$ is the program environment, $\Gamma \vdash x:=v$ means ``the relation $x:=v$ is stored within $\Gamma$,'' and 
$\Gamma \leftarrow x:=v$ means ``store the relation $x:=v$ in $\Gamma$.'' In rule \textsc{E-Seq}, $\Gamma_{|v|}$ denotes all modifications to $\Gamma$ that 
occured during the evaluation of $v$.\\

\begin{tabular}{rlll|l}
$(\lambda x^n.t)v^n$ & $\evals$ & $t[x_i:=v_i]$ &  & \sc{[E-App]} \\
let $(x_i=v_i)^n$ in $t$ & $\evals$ & $t[x_i:=v_i]$ &  & \sc{[E-Let]} \\
define $(x_i=v_i)^n$ & $\evals$ & $\mathtt{nil}$ & $\Gamma \leftarrow (x_i := v_i)$ & \sc{[E-Def]} \\
$x$ & $\evals$ & $v\;\;(\text{if }\Gamma \vdash x := v)$ &  & \sc{[E-Lookup]} \\
match $v_m$ with $(p_i,v_i)^n$ & $\evals$ & $v_k$ &  & \sc{[E-Match1]} \\
default $v_d$ & & \multicolumn{2}{l|}{(if $\exists k$ such that $p_k \models v_m$)} & \\
match $v_m$ with $(p_i,v_i)^n$ & $\evals$ & $v_d$ &  & \sc{[E-Match2]} \\
default $v_d$ & & \multicolumn{2}{l|}{(if $\forall k$, $p_k \not\models v_m$)} & \\
match-dyn $v_m$ with $(p_i,v_i)^n$, & $\evals$ & $v_k$ &  & \sc{[E-Match-Dyn1]} \\
default $v_d$ & & \multicolumn{2}{l|}{(if $\exists k$ such that $p_k \models v_m$)} & \\
match-dyn $v_m$ with $(p_i,v_i)^n$, & $\evals$ & $v_d$ &  & \sc{[E-Match-Dyn2]} \\
default $v_d$ & & \multicolumn{2}{l|}{(if $\forall k$, $p_k \not\models v_m$)} & \\
if $\mfl$ then $v_1$ else $v_2$ & $\evals$ & $v_2$ &  & \sc{[E-If1]} \\
if $\mtr$ then $v_1$ else $v_2$ & $\evals$ & $v_1$ &  & \sc{[E-If2]} \\
if-dyn $\mfl$ then $v_1$ else $v_2$ & $\evals$ & $v_2$ &  & \sc{[E-If-Dyn1]} \\
if-dyn $\mtr$ then $v_1$ else $v_2$ & $\evals$ & $v_1$ &  & \sc{[E-If-Dyn2]} \\
$v_1 \mid v_2$ & $\evals$ & $v_2$ & $\Gamma=\Gamma \cup \Gamma_{|v_1|}$ & \sc{[E-Seq]} \\
\end{tabular}\\
Rules for evaluating primitive operations have been omitted.
\section{Type Rules}

\end{document}
